constR{$x:ut2}(T; c; i) == ([Rinit(i;T;"$x";inl c ); Rframe(i;T;"$x";[])]) 

latex

---

clarification:

constR{$x:ut2}(T; c; i) == ([Rinit(i;T;"$x";inl c ) / [Rframe(i;T;"$x";[]) / []]]) 

latex

Definitions

[], "$x", Rframe(loc;T;x;L), [car / cdr], inl x , Rinit(loc;T;x;v), (L)